$\forall$$T$:Type, $l_{1}$, $l_{2}$, $l_{3}$:$T$ List.
\\[0ex]$l_{1}$ $\leq$ $l_{2}$ @ $l_{3}$ $\Leftrightarrow$ $l_{1}$ $\leq$ $l_{2}$ $\vee$ ($\exists$$l$:$T$ List. 0$<\parallel$$l$$\parallel$ \& $l_{1}$ $=$ ($l_{2}$ @ $l$) \& $l$ $\leq$ $l_{3}$)